COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Richard Statman
C00003 ENDMK
C⊗;
Richard Statman
implicit definability
Beth definability theorem
There is a procedure for finding the explict definition from an
implicit definition.
Prove A(P) ∧ A(Q) ⊃ ∀x.(P x ≡ Q x)